1  /-
  2  Copyright (c) 2019 Johannes Hölzl. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Author: Johannes Hölzl, Casper Putz
  5  
  6  The equivalence between matrices and linear maps.
  7  -/
  8  
  9  import data.matrix.basic
src         └───────────────┘
 10  import linear_algebra.dimension linear_algebra.tensor_product
src         └──────────────────────┘ └───────────────────────────┘
 11  
 12  /-!
 13  
 14  # Linear maps and matrices
 15  
 16  This file defines the maps to send matrices to a linear map,
 17  and to send linear maps between modules with a finite bases
 18  to matrices. This defines a linear equivalence between linear maps
 19  between finite-dimensional vector spaces and matrices indexed by
 20  the respective bases.
 21  
 22  Some results are proved about the linear map corresponding to a
 23  diagonal matrix (range, ker and rank).
 24  
 25  ## Main definitions
 26  
 27  to_lin, to_matrix, linear_equiv_matrix
 28  
 29  ## Tags
 30  
 31  linear_map, matrix, linear_equiv, diagonal
 32  
 33  -/
 34  
 35  noncomputable theory
 36  
 37  open set submodule
 38  
 39  universes u v w
 40  variables {l m n : Type u} [fintype l] [fintype m] [fintype n]
id                               └─────┘     └─────┘     └─────┘
src                              └─────┘     └─────┘     └─────┘
typ                              └─────┘     └─────┘     └─────┘
doc                              └─────┘     └─────┘     └─────┘
 41  
 42  namespace matrix
 43  
 44  variables {R : Type v} [comm_ring R]
id                           └───────┘
src                          └───────┘
typ                          └───────┘
 45  instance [decidable_eq m] [decidable_eq n] (R) [fintype R] : fintype (matrix m n R) :=
id             └──────────┘    └──────────┘        └─────┘     └─────┘  └────┘   
src            └──────────┘     └──────────┘         └─────┘      └─────┘  └────┘
typ            └──────────┘    └──────────┘        └─────┘     └─────┘  └────┘   
doc                                                  └─────┘      └─────┘
 46  by unfold matrix; apply_instance
src     └───────────┘  └──────────────
typ     └───────────┘  └──────────────
doc     └───────────┘  └──────────────
txt     └───────────┘  └──────────────
par     └───────────┘  └──────────────
pid           └─────┘                
st     └──────────────────────────────
 47  
src  
typ  
doc  
txt  
par  
pid  
st   
 48  /-- Evaluation of matrices gives a linear map from matrix m n R to
 49  linear maps (n → R) →ₗ[R] (m → R). -/
 50  def eval : (matrix m n R) →ₗ[R] ((n → R) →ₗ[R] (m → R)) :=
 51  begin
 52    refine linear_map.mk₂ R mul_vec _ _ _ _,
src    └─────┘                      └──────┘
typ    └─────┘                      └──────┘
doc    └─────┘                      └──────┘
txt    └─────┘                      └──────┘
par    └─────┘                      └──────┘
pid                                └──────┘
 53    { assume M N v, funext x,
src      └──────────┘  └──────┘
typ      └──────────┘  └──────┘
doc      └──────────┘  └──────┘
txt      └──────────┘  └──────┘
par      └──────────┘  └──────┘
pid      └──────────┘        └┘
 54      change finset.univ.sum (λy:n, (M x y + N x y) * v y) = _,
src      └─────┘                 └┘ └┘        └┘   └┘ └┘
typ      └─────┘                 └┘ └┘        └┘   └┘ └┘
doc      └─────┘                 └┘ └┘        └┘   └┘ └┘
txt      └─────┘                 └┘ └┘        └┘   └┘ └┘
par      └─────┘                 └┘ └┘        └┘   └┘ └┘
pid                             └┘ └┘        └┘   └┘ └┘
 55      simp only [_root_.add_mul, finset.sum_add_distrib],
src      └─────────┘              └┘                      
typ      └─────────┘              └┘                      
doc      └─────────┘              └┘                      
txt      └─────────┘              └┘                      
par      └─────────┘              └┘                      
pid          └──┘└┘              └┘                      
 56      refl },
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid          
 57    { assume c M v, funext x,
src      └──────────┘  └──────┘
typ      └──────────┘  └──────┘
doc      └──────────┘  └──────┘
txt      └──────────┘  └──────┘
par      └──────────┘  └──────┘
pid      └──────────┘        └┘
st                  └────────┘└─
 58      change finset.univ.sum (λy:n, (c * M x y) * v y) = _,
id              └─────────────┘                  
src      └─────┘└─────────────┘  └┘ └┘      └┘   └┘ └┘
typ      └─────┘└─────────────┘  └┘└┘   └┘  └┘ └┘
doc      └─────┘└─────────────┘  └┘ └┘      └┘   └┘ └┘
txt      └─────┘                 └┘ └┘      └┘   └┘ └┘
par      └─────┘                 └┘ └┘      └┘   └┘ └┘
pid                             └┘ └┘      └┘   └┘ └┘
st   ───────────────────────────────────────────────────────┘└─
 59      simp only [_root_.mul_assoc, finset.mul_sum.symm],
id                  └──────────────┘
src      └─────────┘└──────────────┘└┘                   
typ      └─────────┘└──────────────┘└┘└─────────────────┘
doc      └─────────┘                └┘                   
txt      └─────────┘                └┘                   
par      └─────────┘                └┘                   
pid          └──┘└┘                └┘                   
st   ────────────────────────────────────────────────────┘└─
 60      refl },
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid          
st   ────────┘└┘
 61    { assume M v w, funext x,
src      └──────────┘  └──────┘
typ      └──────────┘  └──────┘
doc      └──────────┘  └──────┘
txt      └──────────┘  └──────┘
par      └──────────┘  └──────┘
pid      └──────────┘        └┘
st   ───┘└──────────┘└────────┘└─
 62      change finset.univ.sum (λy:n, M x y * (v y + w y)) = _,
id              └─────────────┘                   
src      └─────┘└─────────────┘  └┘ └┘          └─┘ └┘
typ      └─────┘└─────────────┘  └┘└┘      └─┘ └┘
doc      └─────┘└─────────────┘  └┘ └┘          └─┘ └┘
txt      └─────┘                 └┘ └┘          └─┘ └┘
par      └─────┘                 └┘ └┘          └─┘ └┘
pid                             └┘ └┘          └─┘ └┘
st   ─────────────────────────────────────────────────────────┘└─
 63      simp [_root_.mul_add, finset.sum_add_distrib],
id             └────────────┘  └────────────────────┘
src      └────┘└────────────┘└┘└────────────────────┘
typ      └────┘└────────────┘└┘└────────────────────┘
doc      └────┘              └┘                      
txt      └────┘              └┘                      
par      └────┘              └┘                      
pid                        └┘                      
st   ────────────────────────────────────────────────┘└─
 64      refl },
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid          
st   ────────┘└┘
 65    { assume c M v, funext x,
src      └──────────┘  └──────┘
typ      └──────────┘  └──────┘
doc      └──────────┘  └──────┘
txt      └──────────┘  └──────┘
par      └──────────┘  └──────┘
pid      └──────────┘        └┘
st   ───────────────┘└────────┘└─
 66      change finset.univ.sum (λy:n, M x y * (c * v y)) = _,
id              └─────────────┘                 
src      └─────┘└─────────────┘  └┘ └┘         └─┘ └┘
typ      └─────┘└─────────────┘  └┘└┘     └─┘ └┘
doc      └─────┘└─────────────┘  └┘ └┘         └─┘ └┘
txt      └─────┘                 └┘ └┘         └─┘ └┘
par      └─────┘                 └┘ └┘         └─┘ └┘
pid                             └┘ └┘         └─┘ └┘
st   ───────────────────────────────────────────────────────┘└─
 67      rw [show (λy:n, M x y * (c * v y)) = (λy:n, c * (M x y * v y)), { funext n, ac_refl },
id                                                           
src      └──┘      └┘ └┘         └─┘   └┘ └┘         └────┘└──────┘└┘└──────┘└──
typ      └──┘      └┘ └┘         └─┘  └┘└┘     └────┘└──────┘└┘└──────┘└──
doc      └──┘      └┘ └┘         └─┘   └┘ └┘         └────┘└──────┘└┘└──────┘└──
txt      └──┘      └┘ └┘         └─┘   └┘ └┘         └────┘└──────┘└┘└──────┘└──
par      └──┘      └┘ └┘         └─┘   └┘ └┘         └────┘└──────┘└┘└──────┘└──
pid        └┘      └┘ └┘         └─┘   └┘ └┘         └──────────────────────────
st   ────────────────────────────────────────────────────────────────────┘└───────┘└────────┘└─
 68        ← finset.mul_sum],
id           └────────────┘
src  ───────┘└────────────┘
typ  ───────┘└────────────┘
doc  ───────┘              
txt  ───────┘              
par  ───────┘              
pid  ───────┘              
st   ─────────────────────┘└──
 69      refl }
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid          
st   ────────┘└─
 70  end
st   ──┘
 71  
 72  /-- Evaluation of matrices gives a map from matrix m n R to
 73  linear maps (n → R) →ₗ[R] (m → R). -/
 74  def to_lin : matrix m n R → (n → R) →ₗ[R] (m → R) := eval.to_fun
id                └────┘            └─┘          └──┘└─────┘
src               └────┘                 └─┘             └──┘└─────┘
typ               └────┘            └─┘          └──┘└─────┘
doc                                                       └──┘
 75  
 76  lemma to_lin_add (M N : matrix m n R) : (M + N).to_lin = M.to_lin + N.to_lin :=
id                           └────┘           └────┘   └─────┘  └─────┘
src                          └────┘                └────┘    └─────┘   └─────┘
typ                          └────┘           └────┘   └─────┘  └─────┘
doc                                                 └────┘     └─────┘    └─────┘
 77  matrix.eval.map_add M N
id   └─────────┘└──────┘  
src  └─────────┘└──────┘
typ  └─────────┘└──────┘  
doc  └─────────┘
 78  
 79  @[simp] lemma to_lin_zero : (0 : matrix m n R).to_lin = 0 :=
id                                    └────┘    └────┘  
src                                   └────┘       └────┘  
typ                                   └────┘    └────┘  
doc    └──┘                                        └────┘
 80  matrix.eval.map_zero
id   └─────────┘└───────┘
src  └─────────┘└───────┘
typ  └─────────┘└───────┘
doc  └─────────┘
 81  
 82  instance to_lin.is_linear_map :
 83    @is_linear_map R (matrix m n R) ((n → R) →ₗ[R] (m → R)) _ _ _ _ _ to_lin :=
id      └───────────┘   └────┘            └─┘                  └────┘
src     └───────────┘    └────┘                 └─┘                     └────┘
typ     └───────────┘   └────┘            └─┘                  └────┘
doc                                                                      └────┘
 84  matrix.eval.is_linear
id   └─────────┘└────────┘
src  └─────────┘└────────┘
typ  └─────────┘└────────┘
doc  └─────────┘
 85  
 86  instance to_lin.is_add_monoid_hom :
 87    @is_add_monoid_hom (matrix m n R) ((n → R) →ₗ[R] (m → R)) _ _ to_lin :=
id      └───────────────┘  └────┘            └─┘            └────┘
src     └───────────────┘  └────┘                 └─┘               └────┘
typ     └───────────────┘  └────┘            └─┘            └────┘
doc     └───────────────┘                                            └────┘
 88  { map_zero := to_lin_zero, map_add := to_lin_add }
id                 └─────────┘             └────────┘
src                └─────────┘             └────────┘
typ                └─────────┘             └────────┘
 89  
 90  @[simp] lemma to_lin_apply (M : matrix m n R) (v : n → R) :
id                                   └────┘             
src                                  └────┘
typ                                  └────┘             
doc    └──┘
 91    (M.to_lin : (n → R) → (m → R)) v = mul_vec M v := rfl
id      └─────┘                   └─────┘      └─┘
src      └─────┘                         └─────┘        └─┘
typ     └─────┘                   └─────┘      └─┘
doc      └─────┘
 92  
 93  lemma mul_to_lin [decidable_eq l] (M : matrix m n R) (N : matrix n l R) :
id                     └──────────┘        └────┘          └────┘   
src                    └──────────┘         └────┘             └────┘
typ                    └──────────┘        └────┘          └────┘   
 94    (M.mul N).to_lin = M.to_lin.comp N.to_lin :=
id      └──┘  └────┘   └─────┘└───┘ └─────┘
src      └──┘   └────┘    └─────┘└───┘  └─────┘
typ     └──┘  └────┘   └─────┘└───┘ └─────┘
doc             └────┘     └─────┘       └─────┘
 95  begin
st   └─────
 96    ext v x,
src    └─────┘
typ    └─────┘
doc    └─────┘
txt    └─────┘
par    └─────┘
pid       └──┘
st   ────────┘└─
 97    simp [to_lin_apply, mul_vec, matrix.mul, finset.sum_mul, finset.mul_sum],
id           └──────────┘  └─────┘  └────────┘  └────────────┘  └────────────┘
src    └────┘└──────────┘└┘└─────┘└┘└────────┘└┘└────────────┘└┘└────────────┘
typ    └────┘└──────────┘└┘└─────┘└┘└────────┘└┘└────────────┘└┘└────────────┘
doc    └────┘            └┘       └┘          └┘              └┘              
txt    └────┘            └┘       └┘          └┘              └┘              
par    └────┘            └┘       └┘          └┘              └┘              
pid                    └┘       └┘          └┘              └┘              
st   ─────────────────────────────────────────────────────────────────────────┘└─
 98    rw [finset.sum_comm],
id         └─────────────┘
src    └──┘└─────────────┘
typ    └──┘└─────────────┘
doc    └──┘               
txt    └──┘               
par    └──┘               
pid      └┘               
st   ────────────────────┘└──
 99    congr, funext x, congr, funext y,
src    └───┘  └──────┘  └───┘  └──────┘
typ    └───┘  └──────┘  └───┘  └──────┘
doc           └──────┘         └──────┘
txt    └───┘  └──────┘  └───┘  └──────┘
par    └───┘  └──────┘  └───┘  └──────┘
pid                 └┘               └┘
st   ──────┘└────────┘└─────┘└────────┘└─
100    rw [mul_assoc]
id         └───────┘
src    └──┘└───────┘└┘
typ    └──┘└───────┘└┘
doc    └──┘         └┘
txt    └──┘         └┘
par    └──┘         └┘
pid      └┘         
st   ──────────────┘
101  end
st   └─┘
102  
103  end matrix
104  
105  namespace linear_map
106  
107  variables {R : Type v} [comm_ring R]
id                           └───────┘
src                          └───────┘
typ                          └───────┘
108  
109  /-- The linear map from linear maps (n → R) →ₗ[R] (m → R) to matrix m n R. -/
110  def to_matrixₗ [decidable_eq n] : ((n → R) →ₗ[R] (m → R)) →ₗ[R] matrix m n R :=
id                   └──────────┘            └─┘        └─┘ └────┘   
src                  └──────────┘               └─┘           └─┘  └────┘
typ                  └──────────┘            └─┘        └─┘ └────┘   
111  begin
st   └─────
112    refine linear_map.mk (λ f i j, f (λ n, ite (j = n) 1 0) i) _ _,
id            └───────────┘                   └─┘    
src    └─────┘└───────────┘  └──────┘   └──┘└─┘   └─────┘ └───┘
typ    └─────┘└───────────┘  └──────┘   └──┘└─┘   └─────┘ └───┘
doc    └─────┘               └──────┘   └──┘       └─────┘ └───┘
txt    └─────┘               └──────┘   └──┘       └─────┘ └───┘
par    └─────┘               └──────┘   └──┘       └─────┘ └───┘
pid                         └──────┘   └──┘       └─────┘ └───┘
st   ───────────────────────────────────────────────────────────────┘└─
113    { assume f g, simp only [add_apply], refl },
id                              └───────┘
src      └────────┘  └─────────┘└───────┘  └───┘
typ      └────────┘  └─────────┘└───────┘  └───┘
doc      └────────┘  └─────────┘           └───┘
txt      └────────┘  └─────────┘           └───┘
par      └────────┘  └─────────┘           └───┘
pid      └────────┘      └──┘└┘               
st   ───┘└────────┘└─────────────────────┘└─────┘└┘
114    { assume f g, simp only [smul_apply], refl }
id                              └────────┘
src      └────────┘  └─────────┘└────────┘  └───┘
typ      └────────┘  └─────────┘└────────┘  └───┘
doc      └────────┘  └─────────┘            └───┘
txt      └────────┘  └─────────┘            └───┘
par      └────────┘  └─────────┘            └───┘
pid      └────────┘      └──┘└┘                
st   ─────────────┘└──────────────────────┘└─────┘└─
115  end
st   ──┘
116  
117  /-- The map from linear maps (n → R) →ₗ[R] (m → R) to matrix m n R. -/
118  def to_matrix [decidable_eq n] : ((n → R) →ₗ[R] (m → R)) → matrix m n R := to_matrixₗ.to_fun
id                  └──────────┘            └─┘          └────┘       └────────┘└─────┘
src                 └──────────┘               └─┘             └────┘          └────────┘└─────┘
typ                 └──────────┘            └─┘          └────┘       └────────┘└─────┘
doc                                                                             └────────┘
119  
120  end linear_map
121  
122  section linear_equiv_matrix
123  
124  variables {R : Type v} [comm_ring R] [decidable_eq n]
id                          └───────┘     └──────────┘
src                          └───────┘     └──────────┘
typ                         └───────┘     └──────────┘
125  
126  open finsupp matrix linear_map
127  
128  /-- to_lin is the left inverse of to_matrix. -/
129  lemma to_matrix_to_lin {f : (n → R) →ₗ[R] (m → R)} :
id                                     └─┘     
src                                      └─┘ 
typ                                    └─┘     
130    to_lin (to_matrix f) = f :=
id     └────┘  └───────┘    
src    └────┘  └───────┘    
typ    └────┘  └───────┘    
doc    └────┘  └───────┘
131  begin
st   └─────
132    ext : 1,
src    └─────┘
typ    └─────┘
doc    └─────┘
txt    └─────┘
par    └─────┘
pid       └┘
st   ────────┘└─
133    -- Show that the two sides are equal by showing that they are equal on a basis
st   ─────────────────────────────────────────────────────────────────────────────────
134    convert linear_eq_on (set.range _) _ (is_basis.mem_span (@pi.is_basis_fun R n _ _) _),
id             └──────────┘  └───────┘       └───────────────┘   └─────────────┘  
src    └──────┘└──────────┘ └───────┘└────┘ └───────────────┘  └─────────────┘  └──────┘
typ    └──────┘└──────────┘ └───────┘└────┘ └───────────────┘  └─────────────┘└──────┘
doc    └──────┘             └───────┘└────┘                                     └──────┘
txt    └──────┘                      └────┘                                     └──────┘
par    └──────┘                      └────┘                                     └──────┘
pid                                 └────┘                                     └──────┘
st   ──────────────────────────────────────────────────────────────────────────────────────┘└─
135    assume e he,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid    └─────────┘
st   ────────────┘└─
136    rw [@std_basis_eq_single R _ _ _ 1] at he,
id          └─────────────────┘ 
src    └──┘ └─────────────────┘ └─────────────┘
typ    └──┘ └─────────────────┘└─────────────┘
doc    └──┘                     └─────────────┘
txt    └──┘                     └─────────────┘
par    └──┘                     └─────────────┘
pid      └┘                     └───────┘└────┘
st   ──────────────────────────────────┘└┘└────┘└─
137    cases (set.mem_range.mp he) with i h,
id            └──────────────┘ └┘
src    └────┘ └──────────────┘  └────────┘
typ    └────┘ └──────────────┘└┘└────────┘
doc    └────┘                   └────────┘
txt    └────┘                   └────────┘
par    └────┘                   └────────┘
pid                            └───────┘
st   ─────────────────────────────────────┘└─
138    ext j,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid       └┘
st   ──────┘└─
139    change finset.univ.sum (λ k, (f.to_fun (λ l, ite (k = l) 1 0)) j * (e k)) = _,
id            └─────────────┘        └──────┘       └─┘                 
src    └─────┘└─────────────┘  └──┘ └──────┘  └──┘└─┘   └──────┘    └─┘ └┘
typ    └─────┘└─────────────┘  └──┘ └──────┘  └──┘└─┘   └──────┘  └─┘ └┘
doc    └─────┘└─────────────┘  └──┘           └──┘       └──────┘     └─┘ └┘
txt    └─────┘                 └──┘           └──┘       └──────┘     └─┘ └┘
par    └─────┘                 └──┘           └──┘       └──────┘     └─┘ └┘
pid                           └──┘           └──┘       └──────┘     └─┘ └┘
st   ──────────────────────────────────────────────────────────────────────────────┘└─
140    rw [←h],
id          
src    └───┘ 
typ    └───┘
doc    └───┘ 
txt    └───┘ 
par    └───┘ 
pid      └─┘ 
st   ───────┘└──
141    conv_lhs { congr, skip, funext,
src    └─────────┘└───┘└┘└──┘└┘└────┘└─
typ    └─────────┘└───┘└┘└──┘└┘└────┘└─
txt    └─────────┘└───┘└┘└──┘└┘└────┘└─
par    └─────────┘└───┘└┘└──┘└┘└────┘└─
pid            └──────────────────────
st   ───────────┘└────┘└────┘└──────┘└─
142      rw [mul_comm, ←smul_eq_mul, ←pi.smul_apply, ←linear_map.smul],
id           └──────┘   └─────────┘   └───────────┘   └─────────────┘
src  ───┘└──┘└──────┘└─┘└─────────┘└─┘└───────────┘└─┘└─────────────┘└─
typ  ───┘└──┘└──────┘└─┘└─────────┘└─┘└───────────┘└─┘└─────────────┘└─
txt  ───┘└──┘        └─┘           └─┘             └─┘               └─
par  ───┘└──┘        └─┘           └─┘             └─┘               └─
pid  ───────┘        └─┘           └─┘             └─┘               └──
st   ───────────────┘└────────────┘└──────────────┘└────────────────┘ └─
143      rw [show _ = ite (i = k) (1:R) 0, by convert single_apply],
id                   └─┘                          └──────────┘
src  ───┘└──┘    └─┘ └─┘    └┘ └┘ └──────┘└──────┘└──────────┘└─
typ  ───┘└──┘    └─┘└─┘  └┘ └┘└──────┘└──────┘└──────────┘└─
doc                                           └──────┘
txt  ───┘└──┘    └─┘        └┘ └┘ └──────┘└──────┘            └─
par  ───┘└──┘    └─┘        └┘ └┘ └──────┘└──────┘            └─
pid  ───────┘    └─┘        └┘ └┘ └──────────────┘            └──
st   ───────────────────────────────────────┘└───────────────────┘ └─
144      rw [show f.to_fun (ite (i = k) (1:R) 0 • (λ l, ite (k = l) 1 0)) = ite (i = k) (f.to_fun _) 0,
id                                                                       └─┘        └──────┘
src  ───┘└──┘                    └┘ └┘ └──┘  └──┘       └──────┘ └─┘    └┘ └──────┘└──────
typ  ───┘└──┘                    └┘ └┘└──┘  └──┘       └──────┘└─┘  └┘ └──────┘└──────
txt  ───┘└──┘                    └┘ └┘ └──┘   └──┘       └──────┘        └┘         └──────
par  ───┘└──┘                    └┘ └┘ └──┘   └──┘       └──────┘        └┘         └──────
pid  ───────┘                    └┘ └┘ └──┘   └──┘       └──────┘        └┘         └──────
st   ───────────────────────────────────────────────────────────────────────────────────────────────────
145        { split_ifs, { rw [one_smul] }, { rw [zero_smul], exact linear_map.map_zero f } }] },
id                            └──────┘           └───────┘         └─────────────────┘ 
src  ───────┘└───────┘└──┘└──┘└──────┘└┘└───┘└──┘└───────┘└┘└────┘└─────────────────┘ └───┘
typ  ───────┘└───────┘└──┘└──┘└──────┘└┘└───┘└──┘└───────┘└┘└────┘└─────────────────┘└───┘
doc          └───────┘    └──┘        └┘     └──┘           └────┘                    
txt  ───────┘└───────┘└──────┘        └─────────┘         └─┘└────┘                    └───┘
par  ───────┘└───────┘└──┘└──┘        └┘└───┘└──┘         └┘└────┘                    └───┘
pid  ────────────────────────┘        └─────────┘         └───────┘                    └─────┘
st   ──────┘└────────┘└─┘└───────────┘└───────────────┘└─────────────────────────────┘└──┘└┘
146    convert finset.sum_eq_single i _ _,
id             └──────────────────┘ 
src    └──────┘└──────────────────┘ └──┘
typ    └──────┘└──────────────────┘└──┘
doc    └──────┘                     └──┘
txt    └──────┘                     └──┘
par    └──────┘                     └──┘
pid                                └──┘
st   ───────────────────────────────────┘└─
147    { rw [if_pos rfl], convert rfl, ext, congr },
id           └────┘ └─┘           └─┘
src      └──┘└────┘└─┘  └──────┘└─┘  └─┘  └────┘
typ      └──┘└────┘└─┘  └──────┘└─┘  └─┘  └────┘
doc      └──┘           └──────┘     └─┘
txt      └──┘           └──────┘     └─┘  └────┘
par      └──┘           └──────┘     └─┘  └────┘
pid        └┘                                 
st   ───┘└────────────┘└────────────┘└───┘└──────┘└┘
148    { assume _ _ hbi, rw [if_neg $ ne.symm hbi], refl },
id                           └────┘   └─────┘ └─┘
src      └────────────┘  └──┘└────┘ └─────┘     └───┘
typ      └────────────┘  └──┘└────┘ └─────┘└─┘  └───┘
doc      └────────────┘  └──┘                   └───┘
txt      └────────────┘  └──┘                   └───┘
par      └────────────┘  └──┘                   └───┘
pid      └────────────┘    └┘                       
st   ───┘└────────────┘└────────────────────────┘└──────┘└┘
149    { assume hi, exact false.elim (hi $ finset.mem_univ i) }
id                        └────────┘  └┘   └─────────────┘ 
src      └───────┘  └────┘└────────┘    └─────────────┘ └┘
typ      └───────┘  └────┘└────────┘ └┘ └─────────────┘└┘
doc      └───────┘  └────┘                              └┘
txt      └───────┘  └────┘                              └┘
par      └───────┘  └────┘                              └┘
pid      └───────┘                                     
st   ────────────┘└──────────────────────────────────────────┘└─
150  end
st   ──┘
151  
152  /-- to_lin is the right inverse of to_matrix. -/
153  lemma to_lin_to_matrix {M : matrix m n R} : to_matrix (to_lin M) = M :=
id                               └────┘       └───────┘  └────┘    
src                              └────┘          └───────┘  └────┘    
typ                              └────┘       └───────┘  └────┘    
doc                                              └───────┘  └────┘
154  begin
st   └─────
155    ext,
src    └─┘
typ    └─┘
doc    └─┘
txt    └─┘
par    └─┘
st   ────┘└─
156    change finset.univ.sum (λ y, M i y * ite (j = y) 1 0) = M i j,
id            └─────────────┘              └─┘                 
src    └─────┘└─────────────┘  └──┘   └─┘   └─────┘   
typ    └─────┘└─────────────┘  └──┘   └─┘   └─────┘ 
doc    └─────┘└─────────────┘  └──┘           └─────┘   
txt    └─────┘                 └──┘           └─────┘   
par    └─────┘                 └──┘           └─────┘   
pid                           └──┘           └─────┘   
st   ──────────────────────────────────────────────────────────────┘└─
157    have h1 : (λ y, M i y * ite (j = y) 1 0) = (λ y, ite (j = y) (M i y) 0),
id                                                      └─┘          
src    └────────┘  └──┘           └─────┘   └──┘└─┘    └┘    └──┘
typ    └────────┘  └──┘           └─────┘   └──┘└─┘   └┘  └──┘
doc    └────────┘  └──┘           └─────┘   └──┘       └┘    └──┘
txt    └────────┘  └──┘           └─────┘   └──┘       └┘    └──┘
par    └────────┘  └──┘           └─────┘   └──┘       └┘    └──┘
pid    └─────┘└─┘  └──┘           └─────┘   └──┘       └┘    └──┘
st   ────────────────────────────────────────────────────────────────────────┘└─
158      { ext, split_ifs, exact mul_one _, exact ring.mul_zero _ },
id                               └─────┘          └───────────┘
src        └─┘  └───────┘  └────┘└─────┘└┘  └────┘└───────────┘└─┘
typ        └─┘  └───────┘  └────┘└─────┘└┘  └────┘└───────────┘└─┘
doc        └─┘  └───────┘  └────┘       └┘  └────┘             └─┘
txt        └─┘  └───────┘  └────┘       └┘  └────┘             └─┘
par        └─┘  └───────┘  └────┘       └┘  └────┘             └─┘
pid                                    └┘                    └┘
st   ─────┘└─┘└─────────┘└───────────────┘└──────────────────────┘└┘
159    have h2 : finset.univ.sum (λ y, ite (j = y) (M i y) 0) = (finset.singleton j).sum (λ y, ite (j = y) (M i y) 0),
id               └─────────────┘                                 └──────────────┘              └─┘          
src    └────────┘└─────────────┘  └──┘       └┘    └───┘  └──────────────┘ └────┘  └──┘└─┘    └┘    └──┘
typ    └────────┘└─────────────┘  └──┘       └┘    └───┘  └──────────────┘ └────┘  └──┘└─┘   └┘  └──┘
doc    └────────┘└─────────────┘  └──┘       └┘    └───┘  └──────────────┘ └────┘  └──┘       └┘    └──┘
txt    └────────┘                 └──┘       └┘    └───┘                   └────┘  └──┘       └┘    └──┘
par    └────────┘                 └──┘       └┘    └───┘                   └────┘  └──┘       └┘    └──┘
pid    └─────┘└─┘                 └──┘       └┘    └───┘                   └────┘  └──┘       └┘    └──┘
st   ───────────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
160      { refine (finset.sum_subset _ _).symm,
id                 └───────────────┘
src        └─────┘ └───────────────┘└────────┘
typ        └─────┘ └───────────────┘└────────┘
doc        └─────┘                  └────────┘
txt        └─────┘                  └────────┘
par        └─────┘                  └────────┘
pid                                └───────┘
st   ─────┘└─────────────────────────────────┘└─
161        { intros _ H, rwa finset.mem_singleton.1 H, exact finset.mem_univ _ },
id                           └──────────────────┘           └─────────────┘
src          └────────┘  └──┘└──────────────────┘└─┘   └────┘└─────────────┘└─┘
typ          └────────┘  └──┘└──────────────────┘└─┘  └────┘└─────────────┘└─┘
doc          └────────┘  └──┘                    └─┘   └────┘               └─┘
txt          └────────┘  └──┘                    └─┘   └────┘               └─┘
par          └────────┘  └──┘                    └─┘   └────┘               └─┘
pid                └──┘                         └─┘                       └┘
st   ───────┘└────────┘└────────────────────────────┘└────────────────────────┘└┘
162        { exact λ _ _ H, if_neg (mt (finset.mem_singleton.2 ∘ eq.symm) H) } },
id                          └────┘  └┘  └──────────────────┘    └─────┘
src          └────┘ └──────┘└────┘ └┘ └──────────────────┘└─┘└─────┘└┘ └┘
typ          └────┘ └──────┘└────┘ └┘ └──────────────────┘└─┘└─────┘└┘ └┘
doc          └────┘ └──────┘                              └─┘        └┘ └┘
txt          └────┘ └──────┘                              └─┘        └┘ └┘
par          └────┘ └──────┘                              └─┘        └┘ └┘
pid                └──────┘                              └─┘        └┘ 
st   ───────────────────────────────────────────────────────────────────────┘└──┘
163    rw [h1, h2, finset.sum_singleton],
id         └┘  └┘  └──────────────────┘
src    └──┘  └┘  └┘└──────────────────┘
typ    └──┘└┘└┘└┘└┘└──────────────────┘
doc    └──┘  └┘  └┘                    
txt    └──┘  └┘  └┘                    
par    └──┘  └┘  └┘                    
pid      └┘  └┘  └┘                    
st   ───────┘└──┘└────────────────────┘└──
164    exact if_pos rfl
id           └────┘ └─┘
src    └────┘└────┘└─┘
typ    └────┘└────┘└─┘
doc    └────┘         
txt    └────┘         
par    └────┘         
pid                  
st   ──────────────────┘
165  end
st   └─┘
166  
167  /-- Linear maps (n → R) →ₗ[R] (m → R) are linearly equivalent to matrix  m n R. -/
168  def linear_equiv_matrix' : ((n → R) →ₗ[R] (m → R)) ≃ₗ[R] matrix m n R :=
id                                     └─┘        └─┘ └────┘   
src                                      └─┘           └─┘  └────┘
typ                                    └─┘        └─┘ └────┘   
doc                                                     └─┘ 
169  { to_fun := to_matrix,
id               └───────┘
src              └───────┘
typ              └───────┘
doc              └───────┘
170    inv_fun := to_lin,
id                └────┘
src               └────┘
typ               └────┘
doc               └────┘
171    right_inv := λ _, to_lin_to_matrix,
id                      └──────────────┘
src                      └──────────────┘
typ                     └──────────────┘
doc                      └──────────────┘
172    left_inv := λ _, to_matrix_to_lin,
id                     └──────────────┘
src                     └──────────────┘
typ                    └──────────────┘
doc                     └──────────────┘
173    add := to_matrixₗ.add,
id            └────────┘└──┘
src           └────────┘└──┘
typ           └────────┘└──┘
doc           └────────┘
174    smul := to_matrixₗ.smul }
id             └────────┘└───┘
src            └────────┘└───┘
typ            └────────┘└───┘
doc            └────────┘
175  
176  /-- Given a basis of two modules M₁ and M₂ over a commutative ring R, we get a linear equivalence
177  between linear maps M₁ →ₗ M₂ and matrices over R indexed by the bases. -/
178  def linear_equiv_matrix {ι κ M₁ M₂ : Type*}
179    [add_comm_group M₁] [module R M₁]
id      └────────────┘ └┘   └────┘  └┘
src     └────────────┘      └────┘
typ     └────────────┘ └┘   └────┘  └┘
doc                         └────┘
180    [add_comm_group M₂] [module R M₂]
id      └────────────┘ └┘   └────┘  └┘
src     └────────────┘      └────┘
typ     └────────────┘ └┘   └────┘  └┘
doc                         └────┘
181    [fintype ι] [decidable_eq ι] [fintype κ] [decidable_eq κ]
id      └─────┘    └──────────┘    └─────┘    └──────────┘ 
src     └─────┘     └──────────┘     └─────┘     └──────────┘
typ     └─────┘    └──────────┘    └─────┘    └──────────┘ 
doc     └─────┘                      └─────┘
182    {v₁ : ι → M₁} {v₂ : κ → M₂} (hv₁ : is_basis R v₁) (hv₂ : is_basis R v₂) :
id              └┘           └┘         └──────┘  └┘         └──────┘  └┘
src                                       └──────┘              └──────┘
typ             └┘           └┘         └──────┘  └┘         └──────┘  └┘
doc                                       └──────┘              └──────┘
183    (M₁ →ₗ[R] M₂) ≃ₗ[R] matrix κ ι R :=
id      └┘ └─┘ └┘  └─┘ └────┘   
src        └─┘      └─┘  └────┘
typ     └┘ └─┘ └┘  └─┘ └────┘   
doc                  └─┘ 
184  linear_equiv.trans (linear_equiv.arrow_congr (equiv_fun_basis hv₁) (equiv_fun_basis hv₂)) linear_equiv_matrix'
id   └────────────────┘  └──────────────────────┘  └─────────────┘ └─┘   └─────────────┘ └─┘   └──────────────────┘
src  └────────────────┘  └──────────────────────┘  └─────────────┘       └─────────────┘       └──────────────────┘
typ  └────────────────┘  └──────────────────────┘  └─────────────┘ └─┘   └─────────────┘ └─┘   └──────────────────┘
doc  └────────────────┘  └──────────────────────┘  └─────────────┘       └─────────────┘       └──────────────────┘
185  
186  end linear_equiv_matrix
187  
188  namespace matrix
189  open_locale matrix
190  
191  section trace
192  
193  variables {R : Type v} {M : Type w} [ring R] [add_comm_group M] [module R M]
id                                        └──┘     └────────────┘     └────┘
src                                       └──┘     └────────────┘     └────┘
typ                                       └──┘     └────────────┘     └────┘
doc                                                                   └────┘
194  
195  /--
196  The diagonal of a square matrix.
197  -/
198  def diag (n : Type u) (R : Type v) (M : Type w)
199    [ring R] [add_comm_group M] [module R M] [fintype n] : (matrix n n M) →ₗ[R] n → M := {
id      └──┘    └────────────┘    └────┘     └─────┘      └────┘     └─┘    
src     └──┘     └────────────┘     └────┘       └─────┘       └────┘        └─┘ 
typ     └──┘    └────────────┘    └────┘     └─────┘      └────┘     └─┘    
doc                                 └────┘       └─────┘
200    to_fun := λ A i, A i i,
id                      
typ                     
201    add    := by { intros, ext, refl, },
src                   └────┘  └─┘  └──┘
typ                   └────┘  └─┘  └──┘
doc                   └────┘  └─┘  └──┘
txt                   └────┘  └─┘  └──┘
par                   └────┘  └─┘  └──┘
st                 └───────┘└───┘└────┘└──┘
202    smul   := by { intros, ext, refl, } }
src                   └────┘  └─┘  └──┘
typ                   └────┘  └─┘  └──┘
doc                   └────┘  └─┘  └──┘
txt                   └────┘  └─┘  └──┘
par                   └────┘  └─┘  └──┘
st                 └───────┘└───┘└────┘└──┘
203  
204  @[simp] lemma diag_one [decidable_eq n] :
id                           └──────────┘ 
src                          └──────────┘
typ                          └──────────┘ 
doc    └──┘
205    diag n R R 1 = λ i, 1 := by { dunfold diag, ext, simp [one_val_eq] }
id     └──┘                                              └────────┘
src    └──┘                         └──────────┘  └─┘  └────┘└────────┘└┘
typ    └──┘                     └──────────┘  └─┘  └────┘└────────┘└┘
doc    └──┘                          └──────────┘  └─┘  └────┘          └┘
txt                                  └──────────┘  └─┘  └────┘          └┘
par                                  └──────────┘  └─┘  └────┘          └┘
pid                                         └───┘                     
st                                └─────────────┘└───┘└──────────────────┘└┘
206  
207  @[simp] lemma diag_transpose (A : matrix n n M) : diag n R M Aᵀ = diag n R M A := rfl
id                                     └────┘       └──┘      └──┘        └─┘
src                                    └────┘          └──┘          └──┘            └─┘
typ                                    └────┘       └──┘      └──┘        └─┘
doc    └──┘                                            └──┘            └──┘
208  
209  /--
210  The trace of a square matrix.
211  -/
212  def trace (n : Type u) (R : Type v) (M : Type w)
213    [ring R] [add_comm_group M] [module R M] [fintype n] : (matrix n n M) →ₗ[R] M := {
id      └──┘    └────────────┘    └────┘     └─────┘      └────┘     └─┘ 
src     └──┘     └────────────┘     └────┘       └─────┘       └────┘        └─┘ 
typ     └──┘    └────────────┘    └────┘     └─────┘      └────┘     └─┘ 
doc                                 └────┘       └─────┘
214    to_fun := finset.univ.sum ∘ (diag n R M),
id               └─────────┘└──┘   └──┘   
src              └─────────┘└──┘   └──┘
typ              └─────────┘└──┘   └──┘   
doc              └─────────┘        └──┘
215    add    := by { intros, apply finset.sum_add_distrib, },
id                                  └────────────────────┘
src                   └────┘  └────┘└────────────────────┘
typ                   └────┘  └────┘└────────────────────┘
doc                   └────┘  └────┘
txt                   └────┘  └────┘
par                   └────┘  └────┘
pid                                
st                 └───────┘└────────────────────────────┘└──┘
216    smul   := by { intros, simp [finset.smul_sum], } }
id                                  └─────────────┘
src                   └────┘  └────┘└─────────────┘
typ                   └────┘  └────┘└─────────────┘
doc                   └────┘  └────┘               
txt                   └────┘  └────┘               
par                   └────┘  └────┘               
pid                                              
st                 └───────┘└──────────────────────┘└──┘
217  
218  @[simp] lemma trace_one [decidable_eq n] :
id                            └──────────┘ 
src                           └──────────┘
typ                           └──────────┘ 
doc    └──┘
219    trace n R R 1 = fintype.card n :=
id     └───┘       └──────────┘ 
src    └───┘          └──────────┘
typ    └───┘       └──────────┘ 
doc    └───┘           └──────────┘
220  have h : trace n R R 1 = finset.univ.sum (diag n R R 1) := rfl,
id            └───┘       └─────────┘└──┘  └──┘          └─┘
src           └───┘          └─────────┘└──┘  └──┘             └─┘
typ           └───┘       └─────────┘└──┘  └──┘          └─┘
doc           └───┘           └─────────┘      └──┘
221  by rw [h, diag_one, finset.sum_const, add_monoid.smul_one]; refl
id            └──────┘  └──────────────┘  └─────────────────┘
src     └──┘ └┘└──────┘└┘└──────────────┘└┘└─────────────────┘  └────
typ     └──┘└┘└──────┘└┘└──────────────┘└┘└─────────────────┘  └────
doc     └──┘ └┘        └┘                └┘                     └────
txt     └──┘ └┘        └┘                └┘                     └────
par     └──┘ └┘        └┘                └┘                     └────
pid       └┘ └┘        └┘                └┘                         
st     └────┘└────────┘└────────────────┘└───────────────────┘└──────
222  
src  
typ  
doc  
txt  
par  
pid  
st   
223  @[simp] lemma trace_transpose (A : matrix n n M) : trace n R M Aᵀ = trace n R M A := rfl
id                                      └────┘       └───┘      └───┘        └─┘
src                                     └────┘          └───┘          └───┘            └─┘
typ                                     └────┘       └───┘      └───┘        └─┘
doc    └──┘                                             └───┘            └───┘
224  
225  @[simp] lemma trace_transpose_mul [decidable_eq n] (A : matrix m n R) (B : matrix n m R) :
id                                      └──────────┘        └────┘          └────┘   
src                                     └──────────┘         └────┘             └────┘
typ                                     └──────────┘        └────┘          └────┘   
doc    └──┘
226    trace n R R (Aᵀ ⬝ Bᵀ) = trace m R R (A ⬝ B) := finset.sum_comm
id     └───┘          └───┘            └─────────────┘
src    └───┘               └───┘                 └─────────────┘
typ    └───┘          └───┘            └─────────────┘
doc    └───┘                   └───┘
227  
228  lemma trace_mul_comm {S : Type v} [comm_ring S] [decidable_eq n]
id                                      └───────┘    └──────────┘ 
src                                     └───────┘     └──────────┘
typ                                     └───────┘    └──────────┘ 
229    (A : matrix m n S) (B : matrix n m S) :
id          └────┘          └────┘   
src         └────┘             └────┘
typ         └────┘          └────┘   
230    trace n S S (B ⬝ A) = trace m S S (A ⬝ B) :=
id     └───┘          └───┘       
src    └───┘               └───┘          
typ    └───┘          └───┘       
doc    └───┘                 └───┘
231  by rw [←trace_transpose, ←trace_transpose_mul, transpose_mul]
id           └─────────────┘   └─────────────────┘  └───────────┘
src     └───┘└─────────────┘└─┘└─────────────────┘└┘└───────────┘└─
typ     └───┘└─────────────┘└─┘└─────────────────┘└┘└───────────┘└─
doc     └───┘               └─┘                   └┘             └─
txt     └───┘               └─┘                   └┘             └─
par     └───┘               └─┘                   └┘             └─
pid       └─┘               └─┘                   └┘             
st     └───────────────────┘└────────────────────┘└─────────────┘
232  
src  
typ  
doc  
txt  
par  
pid  
st   
233  end trace
234  
235  section ring
236  
237  variables {R : Type v} [comm_ring R]
id                           └───────┘
src                          └───────┘
typ                          └───────┘
238  open linear_map matrix
239  
240  lemma proj_diagonal [decidable_eq m] (i : m) (w : m → R) :
id                        └──────────┘                  
src                       └──────────┘
typ                       └──────────┘                  
241    (proj i).comp (to_lin (diagonal w)) = (w i) • proj i :=
id      └──┘  └──┘   └────┘  └──────┘          └──┘ 
src     └──┘   └──┘   └────┘  └──────┘             └──┘
typ     └──┘  └──┘   └────┘  └──────┘          └──┘ 
doc     └──┘          └────┘                         └──┘
242  by ext j; simp [mul_vec_diagonal]
id                   └──────────────┘
src     └───┘  └────┘└──────────────┘└─
typ     └───┘  └────┘└──────────────┘└─
doc     └───┘  └────┘                └─
txt     └───┘  └────┘                └─
par     └───┘  └────┘                └─
pid        └┘                      
st     └───────────────────────────────
243  
src  
typ  
doc  
txt  
par  
pid  
st   
244  lemma diagonal_comp_std_basis [decidable_eq n] (w : n → R) (i : n) :
id                                  └──────────┘                  
src                                 └──────────┘
typ                                 └──────────┘                  
245    (diagonal w).to_lin.comp (std_basis R (λ_:n, R) i) = (w i) • std_basis R (λ_:n, R) i :=
id      └──────┘  └────┘ └──┘   └───────┘                  └───────┘          
src     └──────┘   └────┘ └──┘   └───────┘                        └───────┘
typ     └──────┘  └────┘ └──┘   └───────┘                  └───────┘          
doc                └────┘        └───────┘                          └───────┘
246  begin
st   └─────
247    ext a j,
src    └─────┘
typ    └─────┘
doc    └─────┘
txt    └─────┘
par    └─────┘
pid       └──┘
st   ────────┘└─
248    simp only [linear_map.comp_apply, smul_apply, to_lin_apply, mul_vec_diagonal, smul_apply,
id                └───────────────────┘  └────────┘  └──────────┘  └──────────────┘  └────────┘
src    └─────────┘└───────────────────┘└┘└────────┘└┘└──────────┘└┘└──────────────┘└┘└────────┘└─
typ    └─────────┘└───────────────────┘└┘└────────┘└┘└──────────┘└┘└──────────────┘└┘└────────┘└─
doc    └─────────┘                     └┘          └┘            └┘                └┘          └─
txt    └─────────┘                     └┘          └┘            └┘                └┘          └─
par    └─────────┘                     └┘          └┘            └┘                └┘          └─
pid        └──┘└┘                     └┘          └┘            └┘                └┘          └─
st   ────────────────────────────────────────────────────────────────────────────────────────────
249      pi.smul_apply, smul_eq_mul],
id       └───────────┘  └─────────┘
src  ───┘└───────────┘└┘└─────────┘
typ  ───┘└───────────┘└┘└─────────┘
doc  ───┘             └┘           
txt  ───┘             └┘           
par  ───┘             └┘           
pid  ───┘             └┘           
st   ──────────────────────────────┘└─
250    by_cases i = j,
id                
src    └───────┘ 
typ    └───────┘
doc    └───────┘  
txt    └───────┘  
par    └───────┘  
pid              
st   ───────────────┘└─
251    { subst h },
id             
src      └────┘ 
typ      └────┘
doc      └────┘ 
txt      └────┘ 
par      └────┘ 
pid            
st   ───┘└──────┘└┘
252    { rw [std_basis_ne R (λ_:n, R) _ _ (ne.symm h), _root_.mul_zero, _root_.mul_zero] }
id           └──────────┘                └─────┘    └─────────────┘  └─────────────┘
src      └──┘└──────────┘   └┘ └┘ └────┘ └─────┘ └─┘└─────────────┘└┘└─────────────┘└┘
typ      └──┘└──────────┘   └┘└┘└────┘ └─────┘└─┘└─────────────┘└┘└─────────────┘└┘
doc      └──┘               └┘ └┘ └────┘         └─┘               └┘               └┘
txt      └──┘               └┘ └┘ └────┘         └─┘               └┘               └┘
par      └──┘               └┘ └┘ └────┘         └─┘               └┘               └┘
pid        └┘               └┘ └┘ └────┘         └─┘               └┘               
st   ───────────────────────────────────────────────┘└───────────────┘└───────────────┘└─
253  end
st   ──┘
254  
255  end ring
256  
257  section vector_space
258  
259  variables {K : Type u} [discrete_field K] -- maybe try to relax the universe constraint
id                           └────────────┘
src                          └────────────┘
typ                          └────────────┘
260  
261  open linear_map matrix
262  
263  lemma rank_vec_mul_vec [decidable_eq n] (w : m → K) (v : n → K) :
id                           └──────────┘                     
src                          └──────────┘
typ                          └──────────┘                     
264    rank (vec_mul_vec w v).to_lin ≤ 1 :=
id     └──┘  └─────────┘   └────┘  
src    └──┘  └─────────┘     └────┘  
typ    └──┘  └─────────┘   └────┘  
doc                          └────┘
265  begin
st   └─────
266    rw [vec_mul_vec_eq, mul_to_lin],
id         └────────────┘  └────────┘
src    └──┘└────────────┘└┘└────────┘
typ    └──┘└────────────┘└┘└────────┘
doc    └──┘              └┘          
txt    └──┘              └┘          
par    └──┘              └┘          
pid      └┘              └┘          
st   ───────────────────┘└──────────┘└──
267    refine le_trans (rank_comp_le1 _ _) _,
id            └──────┘  └───────────┘
src    └─────┘└──────┘ └───────────┘└─────┘
typ    └─────┘└──────┘ └───────────┘└─────┘
doc    └─────┘                      └─────┘
txt    └─────┘                      └─────┘
par    └─────┘                      └─────┘
pid                                └─────┘
st   ──────────────────────────────────────┘└─
268    refine le_trans (rank_le_domain _) _,
id            └──────┘  └────────────┘
src    └─────┘└──────┘ └────────────┘└───┘
typ    └─────┘└──────┘ └────────────┘└───┘
doc    └─────┘                       └───┘
txt    └─────┘                       └───┘
par    └─────┘                       └───┘
pid                                 └───┘
st   ─────────────────────────────────────┘└─
269    rw [dim_fun', ← cardinal.fintype_card],
id         └──────┘    └───────────────────┘
src    └──┘└──────┘└──┘└───────────────────┘
typ    └──┘└──────┘└──┘└───────────────────┘
doc    └──┘        └──┘                     
txt    └──┘        └──┘                     
par    └──┘        └──┘                     
pid      └┘        └──┘                     
st   ─────────────┘└───────────────────────┘└──
270    exact le_refl _
id           └─────┘
src    └────┘└─────┘└─┘
typ    └────┘└─────┘└─┘
doc    └────┘       └─┘
txt    └────┘       └─┘
par    └────┘       └─┘
pid                └┘
st   ─────────────────┘
271  end
st   └─┘
272  
273  set_option class.instance_max_depth 100
doc             └──────────────────────┘
274  
275  lemma diagonal_to_lin [decidable_eq m] (w : m → K) :
id                          └──────────┘           
src                         └──────────┘
typ                         └──────────┘           
276    (diagonal w).to_lin = linear_map.pi (λi, w i • linear_map.proj i) :=
id      └──────┘  └────┘   └───────────┘        └─────────────┘ 
src     └──────┘   └────┘   └───────────┘           └─────────────┘
typ     └──────┘  └────┘   └───────────┘        └─────────────┘ 
doc                └────┘    └───────────┘            └─────────────┘
277  by ext v j; simp [mul_vec_diagonal]
id                     └──────────────┘
src     └─────┘  └────┘└──────────────┘└─
typ     └─────┘  └────┘└──────────────┘└─
doc     └─────┘  └────┘                └─
txt     └─────┘  └────┘                └─
par     └─────┘  └────┘                └─
pid        └──┘                      
st     └─────────────────────────────────
278  
src  
typ  
doc  
txt  
par  
pid  
st   
279  lemma ker_diagonal_to_lin [decidable_eq m] (w : m → K) :
id                              └──────────┘           
src                             └──────────┘
typ                             └──────────┘           
280    ker (diagonal w).to_lin = (⨆i∈{i | w i = 0 }, range (std_basis K (λi, K) i)) :=
id     └─┘  └──────┘  └────┘               └───┘  └───────┘        
src    └─┘  └──────┘   └────┘                   └───┘  └───────┘
typ    └─┘  └──────┘  └────┘               └───┘  └───────┘        
doc    └─┘             └────┘                      └───┘  └───────┘
281  begin
st   └─────
282    rw [← comap_bot, ← infi_ker_proj],
id           └───────┘    └───────────┘
src    └────┘└───────┘└──┘└───────────┘
typ    └────┘└───────┘└──┘└───────────┘
doc    └────┘         └──┘             
txt    └────┘         └──┘             
par    └────┘         └──┘             
pid      └──┘         └──┘             
st   ────────────────┘└───────────────┘└──
283    simp only [comap_infi, (ker_comp _ _).symm, proj_diagonal, ker_smul'],
id                └────────┘   └──────┘            └───────────┘  └───────┘
src    └─────────┘└────────┘└┘ └──────┘└──────────┘└───────────┘└┘└───────┘
typ    └─────────┘└────────┘└┘ └──────┘└──────────┘└───────────┘└┘└───────┘
doc    └─────────┘          └┘         └──────────┘             └┘         
txt    └─────────┘          └┘         └──────────┘             └┘         
par    └─────────┘          └┘         └──────────┘             └┘         
pid        └──┘└┘          └┘         └──────────┘             └┘         
st   ──────────────────────────────────────────────────────────────────────┘└─
284    have : univ ⊆ {i : m | w i = 0} ∪ -{i : m | w i = 0}, { rw set.union_compl_self },
id            └──┘                                         └──────────────────┘
src    └─────┘└──┘ └──┘ └─┘  └──┘└──┘ └─┘   └─┘    └─┘└──────────────────┘
typ    └─────┘└──┘ └──┘ └─┘  └──┘└──┘└─┘  └─┘    └─┘└──────────────────┘
doc    └─────┘      └──┘ └─┘   └──┘   └──┘ └─┘   └─┘    └─┘                    
txt    └─────┘      └──┘ └─┘   └──┘   └──┘ └─┘   └─┘    └─┘                    
par    └─────┘      └──┘ └─┘   └──┘   └──┘ └─┘   └─┘    └─┘                    
pid    └───┘└┘      └──┘ └─┘   └──┘   └──┘ └─┘   └─┘                          
st   ─────────────────────────────────────────────────────┘└──┘└──────────────────────┘└┘
285    exact (supr_range_std_basis_eq_infi_ker_proj K (λi:m, K)
id            └───────────────────────────────────┘         
src    └────┘ └───────────────────────────────────┘   └┘ └┘ └─
typ    └────┘ └───────────────────────────────────┘   └┘└┘└─
doc    └────┘                                         └┘ └┘ └─
txt    └────┘                                         └┘ └┘ └─
par    └────┘                                         └┘ └┘ └─
pid                                                  └┘ └┘ └─
st   ───────────────────────────────────────────────────────────
286      (disjoint_compl {i | w i = 0}) this (finite.of_fintype _)).symm
id        └────────────┘               └──┘  └───────────────┘
src  ───┘ └────────────┘ └──┘   └───┘     └───────────────┘└────────┘
typ  ───┘ └────────────┘ └──┘  └───┘└──┘ └───────────────┘└────────┘
doc  ───┘                └──┘   └───┘                      └────────┘
txt  ───┘                └──┘   └───┘                      └────────┘
par  ───┘                └──┘   └───┘                      └────────┘
pid  ───┘                └──┘   └───┘                      └──────┘└┘
st   ───────────────────────────────────────────────────────────────────┘
287  end
st   └─┘
288  
289  lemma range_diagonal [decidable_eq m] (w : m → K) :
id                         └──────────┘           
src                        └──────────┘
typ                        └──────────┘           
290    (diagonal w).to_lin.range = (⨆ i ∈ {i | w i ≠ 0}, (std_basis K (λi, K) i).range) :=
id      └──────┘  └────┘ └───┘                  └───────┘         └───┘
src     └──────┘   └────┘ └───┘                      └───────┘             └───┘
typ     └──────┘  └────┘ └───┘                  └───────┘         └───┘
doc                └────┘ └───┘                         └───────┘             └───┘
291  begin
st   └─────
292    dsimp only [mem_set_of_eq],
id                 └───────────┘
src    └──────────┘└───────────┘
typ    └──────────┘└───────────┘
doc    └──────────┘             
txt    └──────────┘             
par    └──────────┘             
pid         └───┘└┘             
st   ───────────────────────────┘└─
293    rw [← map_top, ← supr_range_std_basis, map_supr],
id           └─────┘    └──────────────────┘  └──────┘
src    └────┘└─────┘└──┘└──────────────────┘└┘└──────┘
typ    └────┘└─────┘└──┘└──────────────────┘└┘└──────┘
doc    └────┘       └──┘                    └┘        
txt    └────┘       └──┘                    └┘        
par    └────┘       └──┘                    └┘        
pid      └──┘       └──┘                    └┘        
st   ──────────────┘└──────────────────────┘└────────┘└──
294    congr, funext i,
src    └───┘  └──────┘
typ    └───┘  └──────┘
doc           └──────┘
txt    └───┘  └──────┘
par    └───┘  └──────┘
pid                 └┘
st   ──────┘└────────┘└─
295    rw [← linear_map.range_comp, diagonal_comp_std_basis, range_smul'],
id           └───────────────────┘  └─────────────────────┘  └─────────┘
src    └────┘└───────────────────┘└┘└─────────────────────┘└┘└─────────┘
typ    └────┘└───────────────────┘└┘└─────────────────────┘└┘└─────────┘
doc    └────┘                     └┘                       └┘           
txt    └────┘                     └┘                       └┘           
par    └────┘                     └┘                       └┘           
pid      └──┘                     └┘                       └┘           
st   ────────────────────────────┘└───────────────────────┘└───────────┘└──
296  end
st   ──┘
297  
298  lemma rank_diagonal [decidable_eq m] (w : m → K) :
id                        └──────────┘           
src                       └──────────┘
typ                       └──────────┘           
299    rank (diagonal w).to_lin = fintype.card { i // w i ≠ 0 } :=
id     └──┘  └──────┘  └────┘   └──────────┘        
src    └──┘  └──────┘   └────┘   └──────────┘           
typ    └──┘  └──────┘  └────┘   └──────────┘        
doc                     └────┘    └──────────┘
300  begin
st   └─────
301    have hu : univ ⊆ - {i : m | w i = 0} ∪ {i : m | w i = 0}, { rw set.compl_union_self },
id               └──┘                                          └──────────────────┘
src    └────────┘└──┘ └──┘ └─┘  └──┘└──┘ └─┘   └─┘    └─┘└──────────────────┘
typ    └────────┘└──┘ └──┘ └─┘  └──┘└──┘└─┘  └─┘    └─┘└──────────────────┘
doc    └────────┘       └──┘ └─┘   └──┘  └──┘ └─┘   └─┘    └─┘                    
txt    └────────┘       └──┘ └─┘   └──┘  └──┘ └─┘   └─┘    └─┘                    
par    └────────┘       └──┘ └─┘   └──┘  └──┘ └─┘   └─┘    └─┘                    
pid    └─────┘└─┘       └──┘ └─┘   └──┘  └──┘ └─┘   └─┘                          
st   ─────────────────────────────────────────────────────────┘└──┘└──────────────────────┘└┘
302    have hd : disjoint {i : m | w i ≠ 0} {i : m | w i = 0} := (disjoint_compl {i | w i = 0}).symm,
id               └──────┘                                     └────────────┘      
src    └────────┘└──────┘ └──┘ └─┘  └──┘└──┘ └─┘   └─────┘ └────────────┘ └──┘   └───────┘
typ    └────────┘└──────┘ └──┘ └─┘  └──┘└──┘└─┘  └─────┘ └────────────┘ └──┘  └───────┘
doc    └────────┘└──────┘ └──┘ └─┘   └──┘ └──┘ └─┘   └─────┘                └──┘   └───────┘
txt    └────────┘         └──┘ └─┘   └──┘ └──┘ └─┘   └─────┘                └──┘   └───────┘
par    └────────┘         └──┘ └─┘   └──┘ └──┘ └─┘   └─────┘                └──┘   └───────┘
pid    └─────┘└─┘         └──┘ └─┘   └──┘ └──┘ └─┘   └─┘└──┘                └──┘   └──────┘
st   ──────────────────────────────────────────────────────────────────────────────────────────────┘└─
303    have h₁ := supr_range_std_basis_eq_infi_ker_proj K (λi:m, K) hd hu (finite.of_fintype _),
id                └───────────────────────────────────┘           └┘ └┘  └───────────────┘
src    └─────────┘└───────────────────────────────────┘   └┘ └┘ └┘     └───────────────┘└─┘
typ    └─────────┘└───────────────────────────────────┘   └┘└┘└┘└┘└┘ └───────────────┘└─┘
doc    └─────────┘                                        └┘ └┘ └┘                      └─┘
txt    └─────────┘                                        └┘ └┘ └┘                      └─┘
par    └─────────┘                                        └┘ └┘ └┘                      └─┘
pid    └─────┘└─┘                                        └┘ └┘ └┘                      └─┘
st   ─────────────────────────────────────────────────────────────────────────────────────────┘└─
304    have h₂ := @infi_ker_proj_equiv K _ _ (λi:m, K) _ _ _ _ (by simp; apply_instance) hd hu,
id                 └─────────────────┘                                                 └┘ └┘
src    └─────────┘ └─────────────────┘ └───┘  └┘ └┘ └────────┘   └──┘└┘└────────────┘└┘  
typ    └─────────┘ └─────────────────┘ └───┘  └┘└┘└────────┘   └──┘└┘└────────────┘└┘└┘└┘
doc    └─────────┘ └─────────────────┘ └───┘  └┘ └┘ └────────┘   └──┘└┘└────────────┘└┘  
txt    └─────────┘                     └───┘  └┘ └┘ └────────┘   └──┘└┘└────────────┘└┘  
par    └─────────┘                     └───┘  └┘ └┘ └────────┘   └──┘└┘└────────────┘└┘  
pid    └─────┘└─┘                     └───┘  └┘ └┘ └────────┘   └─────────────────────┘  
st   ────────────────────────────────────────────────────────────┘└───────────────────┘└─────┘└─
305    rw [rank, range_diagonal, h₁, ←@dim_fun' K],
id         └──┘  └────────────┘  └┘    └──────┘ 
src    └──┘└──┘└┘└────────────┘└┘  └─┘ └──────┘ 
typ    └──┘└──┘└┘└────────────┘└┘└┘└─┘ └──────┘
doc    └──┘    └┘              └┘  └─┘          
txt    └──┘    └┘              └┘  └─┘          
par    └──┘    └┘              └┘  └─┘          
pid      └┘    └┘              └┘  └─┘          
st   ─────────┘└──────────────┘└──┘└────────────┘└──
306    apply linear_equiv.dim_eq,
id           └─────────────────┘
src    └────┘└─────────────────┘
typ    └────┘└─────────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ──────────────────────────┘└─
307    apply h₂,
src    └────┘
typ    └────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ─────────┘└─
308  end
st   ──┘
309  
310  end vector_space
311  
312  end matrix